Nuprl Lemma : f-rel_wf
11,40
postcript
pdf
es
:ES,
L
:(Id List). fischer(
L
)
(
e1
,
e2
:E. Try(
e1
)
Try(
e2
)
(
e1
<f
e2
))
latex
Definitions
t
T
,
P
&
Q
,
Try(
e
)
,
P
Q
,
A
,
x
:
A
.
B
(
x
)
,
Id
,
loc(
e
)
,
the rcv(wanted message from
e1
to
j
)
,
let
x
,
y
=
A
in
B
(
x
;
y
)
,
x
:
A
B
(
x
)
,
E
,
t
.1
,
(
x
l
)
,
e
loc
e'
,
Type
,
s
=
t
,
(
e
<loc
e'
)
,
left
+
right
,
False
,
A
c
B
,
x
:
A
B
(
x
)
,
,
!Void()
,
f-rel{$z,$wanted}(
es
;
L
;
e1
;
e2
)
,
ES
,
type
List
,
fischer(
L
)
Lemmas
f-try
wf
,
fischer
wf
,
event
system
wf
,
not
wf
,
Id
wf
,
false
wf
,
es-locl
wf
,
es-E
wf
,
es-le
wf
,
f-wanted
wf
,
es-loc
wf
,
l
member
subtype
origin
es:ES, L:(Id List). fischer(L) 
(e1, e2:E. Try(e1) Try(e2) (e1 <f e2 
)) es:ES, L:(Id List). fischer(L) (e1, e2:E. Try(e1) Try(e2) (e1 <f e2 )) T Q
Ax:A. B(x)
B(x) l)
loc e' 
B
B(x)